|
Intuitionistic logic, sometimes more generally called constructive logic, is a system of symbolic logic that differs from classical logic by replacing the traditional concept of truth with the concept of constructive provability. For example, in classical logic, propositional formulae are always assigned a truth value from the two element set of trivial propositions ("true" and "false" respectively) regardless of whether we have direct evidence for either case. In contrast, propositional formulae in intuitionistic logic are ''not'' assigned any definite truth value at all and instead ''only'' considered "true" when we have direct evidence, hence ''proof''. (We can also say, instead of the propositional formula being "true" due to direct evidence, that it is inhabited by a proof in the Curry–Howard sense.) Operations in intuitionistic logic therefore preserve justification, with respect to evidence and provability, rather than truth-valuation. Unproved statements in Intuitionistic logic are not given an intermediate truth value (as is sometimes mistakenly asserted). One can prove that such statements have no third truth value, a result dating back to Glivenko in 1928.〔(Proof that intuitionistic logic has no third truth value, Glivenko 1928 )〕 Instead they remain of unknown truth value, until they are either proved or disproved. Statements are disproved by deducing a contradiction from them. A consequence of this point of view is that intuitionistic logic has no interpretation as a two-valued logic, nor even as a finite-valued logic, in the familiar sense. Although intuitionistic logic retains the trivial propositions from classical logic, each ''proof'' of a propositional formula is considered a valid propositional value, thus by Heyting's notion of propositions-as-sets, propositional formulae are (potentially non-finite) sets of their proofs. From a proof-theoretic perspective, intuitionistic logic is a restriction of classical logic in which the law of excluded middle and double negation elimination are not admitted as axioms. Excluded middle and double negation elimination can still be proved for some propositions on a case by case basis, however, but do not hold universally as they do with classical logic. Several systems of semantics for intuitionistic logic have been studied. One semantics mirrors classical Boolean-valued semantics but uses Heyting algebras in place of Boolean algebras. Another semantics uses Kripke models. Intuitionistic logic is practically useful because its restrictions produce proofs that have the existence property, making it also suitable for other forms of mathematical constructivism. Informally, this means that if there is a constructive proof that an object exists, that constructive proof may be used as an algorithm for generating an example of that object. Formalized intuitionistic logic was originally developed by Arend Heyting to provide a formal basis for Brouwer's programme of intuitionism. ==Syntax== The syntax of formulas of intuitionistic logic is similar to propositional logic or first-order logic. However, intuitionistic connectives are not definable in terms of each other in the same way as in classical logic, hence their choice matters. In intuitionistic propositional logic it is customary to use →, ∧, ∨, ⊥ as the basic connectives, treating ¬''A'' as an abbreviation for . In intuitionistic first-order logic both quantifiers ∃, ∀ are needed. Many tautologies of classical logic can no longer be proved within intuitionistic logic. Examples include not only the law of excluded middle , but also Peirce's law , and even double negation elimination. In classical logic, both and also are theorems. In intuitionistic logic, only the former is a theorem: double negation can be introduced, but it cannot be eliminated. Rejecting may seem strange to those more familiar with classical logic, but proving this propositional formula in intuitionistic logic would require producing a proof for the truth or falsity of ''all possible propositional formulae'', which is impossible for a variety of reasons. Because many classically valid tautologies are not theorems of intuitionistic logic, but all theorems of intuitionistic logic are valid classically, intuitionistic logic can be viewed as a weakening of classical logic, albeit one with many useful properties. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「intuitionistic logic」の詳細全文を読む スポンサード リンク
|